#!/usr/bin/python
"""
Dinesh Weerapurage
dpremala@eecs.utk.edu
04/16/2010

This cnf2dimacs program uses 3-SAT to vertex cover algorithm explained in 
Computers and Intractability: A Guide to the Theory of NP-Completeness
by M. R. Garey and D. S. Johnson 

"""
import sys

class CNF2DIMACS:
    
    def __init__ (self, input="input.cnf", output="output.dim"):
        self.input = input
        self.output = output
        self.v = 0
        self.c = 0
        self.x = []
        self.elements = 0

    """
    cnf2dimacs accepts , DIMACS cnf file format which should have labels 1 to N. 
    """
    def parseInput (self):
        # ignore all comments and processing starts 
        #once we found the line that starts with 'p' 
        fin = open(self.input, "r")
        chunk = fin.readline ()
        comm = chunk.split(" ")
        while (comm[0] != 'p'):
            chunk = fin.readline ()
            comm = chunk.split(" ")

        if (comm[0] == 'p'):
            self.v = int(comm[2])
            self.c = int(comm[3])
            self.x = [0]*self.c

        i = 0
        elements = 0;
        while (chunk):
            chunk = fin.readline ()
            chunk = chunk.strip()
            comm = chunk.split(" ")
            if len(comm) > 1:
                lsize = comm.index('0')
                elements = elements + lsize
                self.x[i] = [0]*lsize
                for j in xrange(lsize):
                    self.x[i][j] = int(comm[j])
                    j = j + 1
                i = i + 1
        # keep track of total elements, we need this to compute edges.  
        self.elements = elements
        fin.close ()


    """
    After reading cnf file , writeOutput writes output in DIMACS format and
    prints correspoinding k value.
    """
    def writeOutput (self):
        values = {}
        fout = open (self.output, "w")
        nodes = 2*self.v + 3*self.c
        edges = self.v + 3*self.c + self.elements

        for i in xrange (1, 2*self.v + 1):
            if i < (self.v + 1):
                values[i] = i 
            else:
                values[self.v - i] = i
        
        line = str(nodes)+"\t"+str(edges)+"\n"
        fout.write(line)

        for i in xrange (1, self.v+1):
            line = str(i)+"\t"+str(values[-i])+"\n"
            fout.write(line)

        for i in xrange (1, self.c+1):
            k = 2*self.v + 3*i
            line = str(k)+"\t"+str(k-1)+"\n"
            fout.write(line)
            line = str(k)+"\t"+str(k-2)+"\n"
            fout.write(line)
            line = str(k-2)+"\t"+str(k-1)+"\n"
            fout.write(line)

        for i in xrange (1, len(self.x) + 1):
            k = 2*self.v + 3*i
            for j in xrange (len(self.x[i-1])):
                line = str(k-j)+"\t"+str(values[self.x[i-1][j]])+"\n"
                fout.write(line)
        fout.close ()
        print "k value for this graph is", (self.v + 2*self.c)

    def outputCNF (self, file):
        f = open(file, "r")
        chunk = f.readline()
        chunk = chunk.strip()
        size = int(chunk)
        array = [0]*size
        i = 0
        chunk = f.readline()
        for i in xrange(size):
            chunk = f.readline()
            chunk = chunk.strip()
            array[i] = int(chunk)
        f.close ()

        values = {}
        for i in xrange (1, 2*self.v + 1):
            if i < (self.v + 1):
                values[i] = i 
            else:
                values[i] = self.v - i

        for i in xrange (size):
            if ((array[i] > 0) and (array[i] < 2*self.v + 1)):
                print values[array[i]]
            


def main ():
    if len (sys.argv) < 3:
        print "usage:"+sys.argv[0]+" <inputfile> <outputfile>\n"
        sys.exit (0);

    input = sys.argv[1]
    output = sys.argv[2]
    cnf = ''

    if len (sys.argv) > 3:
        cnf = sys.argv[3]

    e = CNF2DIMACS(input, output)
    e.parseInput ()

    if (cnf == '-cnf'):
        e.outputCNF(output)
    else:
        e.writeOutput()

        

        

if __name__ == "__main__":
    main ();
